CNR Author
operator:
and / or
Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2016
Conference article
Open Access
A tool-chain for statistical spatio-temporal model checking of bike sharing systems
Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A.
Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution.Source: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A.
Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution.Source: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository 
| doi.org 
| link.springer.com | CNR ExploRA
2016
Report
Open Access
Scalable verification for spatial stochastic logics
Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., Paskauskas R., Tribastone M., Tschaikowski M.
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLSource: ISTI Technical reports, 2016
Project(s): QUANTICOL
Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., Paskauskas R., Tribastone M., Tschaikowski M.
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLSource: ISTI Technical reports, 2016
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2015
Conference article
Open Access
Model-based Assessment of Aspects of User-satisfaction in Bicycle Sharing Systems
Massink M., Pasìoekauskas R.
Modelling of bike sharing systems as Markov Renewal Process is examined with the aim of capturing and assessing various forms of user (dis)satisfaction. A class of models with minimal assumptions about distributions of bicycle parking stations and service requests is developed in which rational commuter behaviour is taken into account. Stochastic time evolution of these models is studied, using a generalised version of Gillespie's exact stochastic integration algorithm that accounts for non-Markovian inter-event times. The model is shown to reproduce quite faithfully the trip-duration statistics of smaller and larger real bike sharing systems, such as those in London and Pisa, including the algebraic 'tails' of these distributions that are made up of longer cycling trips. The latter are related to user's difficulties to find suitable parking places therefore to a potential source of distress. The model also predicts other salient features such as a mode at 10 minutes and crossover behaviour at about 30 minutes. The framework can be extended to include measures either designed to improve, or anyway to affect, the user experience with a system, such as incentives for spontaneous vehicle redistribution. User satisfaction is difficult to assess in real systems because these naturally collect only data about trips that actually, and thus successfully, took place giving only partial and biased insight in user satisfaction.Source: 18th IEEE International Conference on Intelligent Transportation Systems, pp. 1363–1370, Las Palmas de Gran Canaria Canary Islands, Spain, 15-18/09/2015
DOI: 10.1109/itsc.2015.224
Project(s): QUANTICOL
Metrics:
Massink M., Pasìoekauskas R.
Modelling of bike sharing systems as Markov Renewal Process is examined with the aim of capturing and assessing various forms of user (dis)satisfaction. A class of models with minimal assumptions about distributions of bicycle parking stations and service requests is developed in which rational commuter behaviour is taken into account. Stochastic time evolution of these models is studied, using a generalised version of Gillespie's exact stochastic integration algorithm that accounts for non-Markovian inter-event times. The model is shown to reproduce quite faithfully the trip-duration statistics of smaller and larger real bike sharing systems, such as those in London and Pisa, including the algebraic 'tails' of these distributions that are made up of longer cycling trips. The latter are related to user's difficulties to find suitable parking places therefore to a potential source of distress. The model also predicts other salient features such as a mode at 10 minutes and crossover behaviour at about 30 minutes. The framework can be extended to include measures either designed to improve, or anyway to affect, the user experience with a system, such as incentives for spontaneous vehicle redistribution. User satisfaction is difficult to assess in real systems because these naturally collect only data about trips that actually, and thus successfully, took place giving only partial and biased insight in user satisfaction.Source: 18th IEEE International Conference on Intelligent Transportation Systems, pp. 1363–1370, Las Palmas de Gran Canaria Canary Islands, Spain, 15-18/09/2015
DOI: 10.1109/itsc.2015.224
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | ieeexplore.ieee.org | CNR ExploRA
2015
Conference article
Open Access
Exploring spatio-temporal properties of bike-sharing systems
Ciancia V., Latella D., Massink M., Paskauskas R.
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.Source: IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 74–79, Cambridge, MA, USA, 21-25/09/2015
DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Massink M., Paskauskas R.
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.Source: IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 74–79, Cambridge, MA, USA, 21-25/09/2015
DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | ieeexplore.ieee.org | CNR ExploRA
2015
Report
Open Access
Model-based assessment of aspects of user-satisfaction in bicycle sharing systems
Massink M., Paskauskas R.
A simulation model for bike-sharing systems is proposed and results of its use are discussed.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
Massink M., Paskauskas R.
A simulation model for bike-sharing systems is proposed and results of its use are discussed.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2014
Report
Unknown
QUANTICOL - Multiscale modelling informed by smart grids
Gast N., Bortolussi L., Jane H., Paskauskas R., Trinabastone M.
Multiple scales are inherent to collaborative adaptive systems (CAS). They can be temporal, for example, adjusting the production of a large power plant takes hours while appliances can switched on or of the instant a signal is received. They can also be organizational and represent a hierarchical structure, for example a smart building that contains rooms. Fluid approximations, and in particular mean-field limits, are a powerful tool to conduct a quantitative analysis of large stochastic systems. Yet existing techniques are not well adapted to study multiple-scale behaviour. This deliverable reports on Task 1.1 and 1.2 of Work Package 1. We mainly focus on two aspects: (1) how to define and construct mean-field limits in the presence of multiple scales and (2) what approximations are needed to build efficient control algorithms for smart grids. This deliverable presents results from published papers by the members of the project as well as the relevant literature. Our approach is to develop the theory in a way informed by examples. The results presented in this deliverable are motivated by their applicability to model smart grids and smart buildings. Hence, each section contains at least one concrete example of how the results apply to our case-studies. We rst present a review of model reduction techniques in the presence of multiple time scales. This occurs when the states of some objects evolve at a much faster time scale than others (for example, small electric appliances and big power plants). We compare existing reduction techniques for deterministic dynamical systems, a mature subject, with on-going work on stochastic systems. This review shows that a number of time-scale reduction techniques can be readily applied to mean-field models. It gives us tools to develop the analog for stochastic systems. We then describe the situation when there are multiple population scales. Our basic example is when one centralized controller interacts with many appliances. We show that in such cases, the limit is naturally described by a stochastic hybrid system. We describe how to construct the limit and the limitations of the approach. This technique reduces greatly the complexity of the simulation while maintaining a good accuracy. We develop a novel formalism to describe systems of systems. This can model systems that have a hierarchical organization. This formalism allows us to automatically reduce the complexity of the mean-field equations, by exploiting symmetries in the model. This method can be applied iteratively, to construct hierarchical abstractions of systems. We illustrate our method to describe the behaviour of a collection of smart buildings. In the last section, we demonstrate the use of optimization tools for building control algorithms in electrical systems that have a large production of renewable energy. We model and treat two challenges: large forecast uncertainties and presence of delay due to multiple time scales. We study two directions based on centralized and distributed control. We develop storage and demand/response management policies, where a central controller sends signals to smart users to adapt the consumption to the production. These policies are more robust to forecast errors than existing strategies. To conclude, this work package reports on progress that has been made on the fundamental aspects of multi-scale modeling as well as on advances in the smart-grid case study. This constitutes a rst attempt to build generic tools that will be applicable to the analysis and the optimization of the other case studies. We will continue the development of these generic methods to incorporate spatial behaviour (Work Package 2) and apply these techniques to uid model checking (Work Package 3).Source: Project report, QUANTICOL, Deliverable D1.1, 2014
Project(s): QUANTICOL
Gast N., Bortolussi L., Jane H., Paskauskas R., Trinabastone M.
Multiple scales are inherent to collaborative adaptive systems (CAS). They can be temporal, for example, adjusting the production of a large power plant takes hours while appliances can switched on or of the instant a signal is received. They can also be organizational and represent a hierarchical structure, for example a smart building that contains rooms. Fluid approximations, and in particular mean-field limits, are a powerful tool to conduct a quantitative analysis of large stochastic systems. Yet existing techniques are not well adapted to study multiple-scale behaviour. This deliverable reports on Task 1.1 and 1.2 of Work Package 1. We mainly focus on two aspects: (1) how to define and construct mean-field limits in the presence of multiple scales and (2) what approximations are needed to build efficient control algorithms for smart grids. This deliverable presents results from published papers by the members of the project as well as the relevant literature. Our approach is to develop the theory in a way informed by examples. The results presented in this deliverable are motivated by their applicability to model smart grids and smart buildings. Hence, each section contains at least one concrete example of how the results apply to our case-studies. We rst present a review of model reduction techniques in the presence of multiple time scales. This occurs when the states of some objects evolve at a much faster time scale than others (for example, small electric appliances and big power plants). We compare existing reduction techniques for deterministic dynamical systems, a mature subject, with on-going work on stochastic systems. This review shows that a number of time-scale reduction techniques can be readily applied to mean-field models. It gives us tools to develop the analog for stochastic systems. We then describe the situation when there are multiple population scales. Our basic example is when one centralized controller interacts with many appliances. We show that in such cases, the limit is naturally described by a stochastic hybrid system. We describe how to construct the limit and the limitations of the approach. This technique reduces greatly the complexity of the simulation while maintaining a good accuracy. We develop a novel formalism to describe systems of systems. This can model systems that have a hierarchical organization. This formalism allows us to automatically reduce the complexity of the mean-field equations, by exploiting symmetries in the model. This method can be applied iteratively, to construct hierarchical abstractions of systems. We illustrate our method to describe the behaviour of a collection of smart buildings. In the last section, we demonstrate the use of optimization tools for building control algorithms in electrical systems that have a large production of renewable energy. We model and treat two challenges: large forecast uncertainties and presence of delay due to multiple time scales. We study two directions based on centralized and distributed control. We develop storage and demand/response management policies, where a central controller sends signals to smart users to adapt the consumption to the production. These policies are more robust to forecast errors than existing strategies. To conclude, this work package reports on progress that has been made on the fundamental aspects of multi-scale modeling as well as on advances in the smart-grid case study. This constitutes a rst attempt to build generic tools that will be applicable to the analysis and the optimization of the other case studies. We will continue the development of these generic methods to incorporate spatial behaviour (Work Package 2) and apply these techniques to uid model checking (Work Package 3).Source: Project report, QUANTICOL, Deliverable D1.1, 2014
Project(s): QUANTICOL
See at: CNR ExploRA